(declare-fun a () Int)
(assert (= a 0))
(declare-fun Wbase_4_1_12 () Int)
(assert (< Wbase_4_1_12 8))
(declare-fun Wbase_4_2_12 () Int)
(assert (< Wbase_4_2_12 8))
(assert (>= Wbase_4_2_12 0))
(declare-fun Wbase_4_3_12 () Int)
(assert (< Wbase_4_3_12 8))
(assert (>= Wbase_4_3_12 0))
(declare-fun Wbase_2_0_6 () Int)
(assert (< Wbase_2_0_6 8))
(assert (>= Wbase_2_0_6 0))
(declare-fun Wbase_2_1_6 () Int)
(assert (< Wbase_2_1_6 8))
(assert (>= Wbase_2_1_6 0))
(declare-fun Wbase_2_0_14 () Int)
(declare-fun Wbase_2_1_14 () Int)
(assert (< Wbase_2_1_14 8))
(declare-fun Wbase_1_0_3 () Int)
(declare-fun Wbase_1_0_11 () Int)
(declare-fun Wbase_1_0_7 () Int)
(assert (< Wbase_1_0_7 8))
(assert (>= Wbase_1_0_7 0))
(declare-fun Wbase_1_0_15 () Int)
(assert (let ((g 0)(h 0)(i 0)(j 0)(k (+ Wbase_4_1_12 4))) (let ((l (ite (<= k 8) k (- k 8)))(qf Wbase_4_1_12)(m (+ Wbase_4_2_12 4))) (let ((n (ite (<= m 8) m (- m 8)))(o Wbase_4_2_12)(p Wbase_4_3_12)) (let ((q (ite (<= p 8) p (div 96 p 8)))(qi Wbase_4_3_12)(qn (+ Wbase_2_0_6 6))) (let ((qo (ite (<= qn 8) qn (- qn 8)))(qp Wbase_2_0_6)(ql (mod Wbase_2_1_6 6))) (let ((qm (ite true ql 0))(qs Wbase_2_1_6)(qt 6)) (let ((qu (ite true qt 0))(qv Wbase_2_0_14)(qq 6)) (let ((qr (ite true qq 0))(qx Wbase_2_1_14)(qy (+ Wbase_1_0_3 3))) (let ((qad (ite (<= qy 8) qy 0))(qae Wbase_1_0_11)(qaf Wbase_1_0_7)(qag (+ Wbase_1_0_15 7))) (let ((qah (ite (<= qag 8) qag (- 8)))(qai Wbase_1_0_15)(qaj (- Wbase_4_1_12 g))) (let ((qak (ite (< qaj 0) 0 qaj))(qal (- Wbase_4_3_12))) (let ((qam (ite (< qal 0) (+ qal 8) qal))(qan (- l h))) (let ((qao (ite (< qan 0) (+ qan 8) qan))(qz (- n i))) (let ((qap (ite (< qz 0) (+ qz 8) qz))(qaq (- q j))) (let ((qar (ite (< qaq 0) (+ qaq 8) qaq))(qas (- Wbase_2_1_6 Wbase_4_1_12))) (let ((qaz (ite (< qas 0) 8 qas))(qat (- qo Wbase_4_2_12))) (let ((qau (ite (< qat 0) (+ qat 8) qat))(qav (- qm Wbase_4_3_12))) (let ((qaw (ite (< qav 0) (+ qav 8) qav))(qax (- Wbase_2_1_14 qf))) (let ((qay (ite (< qax 0) (+ qax 8) qax))(qbi (- qu o))) (let ((qba (ite (< qbi 0) 0 qbi))(qbb (- qr qi))) (let ((qbc (ite (< qbb 0) (+ qbb 8) qbb))(qbd (- qad Wbase_2_1_6))) (let ((qbe (ite (< qbd 0) (+ qbd 8) qbd))(qbf (- Wbase_1_0_11 qp))) (let ((qbg (ite (< qbf 0) (+ qbf 8) qbf))(qbh (- qs))) (let ((qbt (ite (< qbh 0) (+ qbh 8) qbh))(qbj (- Wbase_1_0_15 qv))) (let ((qbk (ite (< qbj 0) (+ qbj 8) qbj))(qbl (- qah qx))) (let ((qbm (ite (< qbl 0) (+ qbl 8) qbl))(qbn qae)) (let ((qbo (ite (< qbn 0) (+ qbn 8) qbn))(qbp (- Wbase_1_0_7))) (let ((qbq (ite (< qbp 0) (+ qbp 8) qbp))(qbr (- qaf))) (let ((qbs (ite (< qbr 0) (+ qbr 8) qbr))(qcl (- qai))) (let ((qbu (ite true qcl qcl))(qbv (= qak 0))(qbw (= qak 4))) (let ((qbx (ite qbv 0 (ite qbw 2 3)))(qby (= qam 0))(qbz (= qam 4))) (let ((qca (ite qby 0 (ite qbz 2 3)))(qcb (= qao 0))(qcc (= qao 4))) (let ((qcd (ite qcb 0 (ite qcc 2 3)))(qce (= qap 0))(qcf (= qap 4))) (let ((qcg (ite qce 0 (ite qcf 2 3)))(qch (= qar 0))(qci (= qar 4))) (let ((qcj (ite qch 0 (ite qci 2 3)))(qck (= qaz 0))(qdg (= qaz 4))) (let ((qcm (ite qck 0 (ite qdg 2 3)))(qcn (= qau 0))(qco (= qau 4))) (let ((qcp (ite qcn 0 (ite qco 2 3)))(qcq (= qaw 0))(qcr (= qaw 4))) (let ((qcs (ite qcq 0 (ite qcr 2 3)))(qct (= qay 0))(qcu (= qay 4))) (let ((qcv (ite qct 0 (ite qcu 2 3)))(qcw (= qba 0))(qcx (= qba 4))) (let ((qcy (ite qcw 0 (ite qcx 2 3)))(qcz (= qbc 0))(qda (= qbc 4))) (let ((qdb (ite qcz 0 (ite qda 2 3)))(qdc (= qbe 0))(c (= qbe 4))) (let ((qde (ite qdc 0 (ite c 2 3)))(qed (= qbg 0))(qdf (= qbg 4))) (let ((qef (ite qed 0 (ite qdf 2 3)))(qdh (= qbt 0))(qdi (= qbt 4))) (let ((qei (ite qdh 0 (ite qdi 2 3)))(qdj (= qbk 0))(qdk (= qbk 4))) (let ((qdl (ite qdj 0 (ite qdk 2 3)))(qdm (= qbm 0))(qdn (= qbm 4))) (let ((qdo (ite qdm 0 (ite qdn 2 3)))(qdp (= qbo 0))(qdq (= qbo 4))) (let ((qdr (ite qdp 0 (ite qdq 2 3)))) (let ((qds qdr)(qdt (= qbq 0))(qdu (= qbq 4))) (let ((qdv (ite qdt 0 (ite qdu 2 3)))) (let ((qdw qdv)(qdx (= qbs 0))(qdy (= qbs 4))) (let ((qdz (ite qdx 0 (ite qdy 2 3)))) (let ((qea qdz)(qeb (= qbu 0))(qec (= qbu 4))) (let ((qfi (ite qeb 0 (ite qec 2 3)))) (let ((qee qfi)(qfj qde)) (let ((qeg qfj)(qeh qds)(qfk (+ qef qei))) (let ((qej (+ qfk qeh))) (let ((qek (+ qeg qej))(qel qcp)(qem (+ qcm qcs))) (let ((qw (+ qel qem))) (let ((qen (+ qw qek))(qeo (+ qdw qea))) (let ((qep qeo)(qeq qee)(qer (+ qdl qdo))) (let ((qes (+ qer qeq))) (let ((qet (+ qep qes))(qeu qcy)(qev (+ qcv qdb))) (let ((qew (+ qeu qev))) (let ((qex (+ qew qet))) (let ((qey (<= qex 24))(qez (+ qen qex))(qfa qcg)) (let ((qfb qfa)(qfc (+ qbx qcd))(qfd (+ qca qcj))) (let ((e (+ qfc qfd))) (let ((d (+ qfb e))) (let ((f (+ d qez))) (let ((b (<= f 24))) (and qey b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
